Section: New Results

Composition results (Objective 1)

Participants : Vincent Cheval, Stéphanie Delaune.

Formal methods have proved their usefulness for analysing the security of protocols. However, protocols are often analysed in isolation, and this is well-known to be not sufficient as soon as the protocols share some keys. Nowdays, several composition results exist for trace-based properties, but there is a lack of composition results for equivalence-based properties.

Myrto Arapinis, Vincent Cheval, and Stéphanie Delaune study the notion of trace equivalence and we show how to establish such an equivalence relation in a modular way. They show that composition works even when the processes share secrets provided that they satisfy some reasonable conditions. Their composition result allows one to prove various equivalence-based properties in a modular way, and works in a quite general setting. In particular, they consider arbitrary cryptographic primitives and processes that use non-trivial else branches. As an example, they consider the ICAO e-passport standard, and they show how the privacy guarantees of the whole application can be derived from the privacy guarantees of its sub-protocols. This work was published at CSF'12 [22] .